((VARTYPECTR? . 0) (LISP (NIL . (DECL (U U0 U1 U2 U3 V V0 V1 V2 V3 W W0 W1
W2 W3) (OT& . GROUND) VARIABLE LIST) . NIL . ((W3 . (VARIABLE . GROUND .
LIST . NIL . NIL . 1 . W3 .)) (W1 . (VARIABLE . GROUND . LIST . NIL . NIL
. 1 . W1 .)) (W . (VARIABLE . GROUND . LIST . NIL . NIL . 1 . W .)) (V2 .
(VARIABLE . GROUND . LIST . NIL . NIL . 1 . V2 .)) (V0 . (VARIABLE .
GROUND . LIST . NIL . NIL . 1 . V0 .)) (U3 . (VARIABLE . GROUND . LIST .
NIL . NIL . 1 . U3 .)) (U1 . (VARIABLE . GROUND . LIST . NIL . NIL . 1 .
U1 .)) (U . (VARIABLE . GROUND . LIST . NIL . NIL . 1 . U .)) (LIST .
(VARIABLE . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (4 . LIST . PREFIX .
1000 .) . 1 . LIST .)) (U0 . (VARIABLE . GROUND . LIST . NIL . NIL . 1 .
U0 .)) (U2 . (VARIABLE . GROUND . LIST . NIL . NIL . 1 . U2 .)) (V .
(VARIABLE . GROUND . LIST . NIL . NIL . 1 . V .)) (V1 . (VARIABLE . GROUND
. LIST . NIL . NIL . 1 . V1 .)) (V3 . (VARIABLE . GROUND . LIST . NIL .
NIL . 1 . V3 .)) (W0 . (VARIABLE . GROUND . LIST . NIL . NIL . 1 . W0 .))
(W2 . (VARIABLE . GROUND . LIST . NIL . NIL . 1 . W2 .))) . NIL . NIL .
NIL . NIL . NIL . LISP . NIL . NIL . 1 .) (NIL . (DECL (X Y Z) (OT& .
GROUND) VARIABLE SEXP) . NIL . ((Z . (VARIABLE . GROUND . SEXP . NIL . NIL
. 2 . Z .)) (X . (VARIABLE . GROUND . SEXP . NIL . NIL . 2 . X .)) (SEXP .
(VARIABLE . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (4 . SEXP . PREFIX .
1000 .) . 2 . SEXP .)) (Y . (VARIABLE . GROUND . SEXP . NIL . NIL . 2 . Y
.))) . NIL . NIL . NIL . NIL . NIL . LISP . NIL . NIL . 2 .) (NIL . (DECL
(A B C) (OT& . GROUND) VARIABLE) . NIL . ((C . (VARIABLE . GROUND .
UNIVERSAL . NIL . NIL . 3 . C .)) (A . (VARIABLE . GROUND . UNIVERSAL .
NIL . NIL . 3 . A .)) (B . (VARIABLE . GROUND . UNIVERSAL . NIL . NIL . 3
. B .))) . NIL . NIL . NIL . NIL . NIL . LISP . NIL . NIL . 3 .) (NIL .
(DECL (PHI) (OT& (GROUND) . TRUTHVAL) VARIABLE) . NIL . ((PHI . (VARIABLE
. ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . NIL . 4 . PHI .))) . NIL . NIL
. NIL . NIL . NIL . LISP . NIL . NIL . 4 .) (NIL . (DECL (NNIL) (OT& .
GROUND) CONSTANT LIST) . NIL . ((NNIL . (CONSTANT . GROUND . LIST . NIL .
NIL . 5 . NNIL .)) (LIST . 1)) . NIL . NIL . NIL . NIL . NIL . LISP . NIL
. NIL . 5 .) (NIL . (DECL (CONS) (OT& (GROUND GROUND) . GROUND) CONSTANT)
. NIL . ((CONS . (CONSTANT . ((GROUND GROUND) . GROUND) . UNIVERSAL . NIL
. NIL . 6 . CONS .))) . NIL . NIL . NIL . NIL . NIL . LISP . NIL . NIL . 6
.) (NIL . (DECL (CAR CDR) (OT& (GROUND) . GROUND) CONSTANT) . NIL . ((CDR
. (CONSTANT . ((GROUND) . GROUND) . UNIVERSAL . NIL . NIL . 7 . CDR .))
(CAR . (CONSTANT . ((GROUND) . GROUND) . UNIVERSAL . NIL . NIL . 7 . CAR
.))) . NIL . NIL . NIL . NIL . NIL . LISP . NIL . NIL . 7 .) (NIL . (DECL
(NULL) (OT& (GROUND) . TRUTHVAL) CONSTANT) . NIL . ((NULL . (CONSTANT .
((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . NIL . 8 . NULL .))) . NIL . NIL
. NIL . NIL . NIL . LISP . NIL . NIL . 8 .) (NIL . (DECL (LIST) (OT&
(GROUND) . TRUTHVAL) CONSTANT) . NIL . ((LIST . (CONSTANT . ((GROUND) .
TRUTHVAL) . UNIVERSAL . NIL . NIL . 9 . LIST .))) . NIL . NIL . NIL . NIL
. NIL . LISP . NIL . NIL . 9 .) (NIL . (DECL (SEXP) (OT& (GROUND) .
TRUTHVAL) CONSTANT) . NIL . ((SEXP . (CONSTANT . ((GROUND) . TRUTHVAL) .
UNIVERSAL . NIL . NIL . 10 . SEXP .))) . NIL . NIL . NIL . NIL . NIL .
LISP . NIL . NIL . 10 .) ((((∀ U)) (SEXP U)) . (AXIOM (TM& ((∀ U)) (SEXP
U))) . NIL . ((U . 1) (SEXP . 10)) . NIL . NIL . NIL . (11) . NIL . LISP .
NIL . NIL . 11 .) ((((∀ X U)) (LIST (CONS X U))) . (AXIOM (TM& ((∀ X U))
(LIST (CONS X U)))) . NIL . ((U . 1) (X . 2) (CONS . 6) (LIST . 9)) . NIL
. NIL . NIL . (12) . NIL . LISP . NIL . NIL . 12 .) ((((∀ U)) (≡ (NULL U)
(= U NNIL))) . (AXIOM (TM& ((∀ U)) (≡ (NULL U) (= U NNIL)))) . NIL . ((U .
1) (NNIL . 5) (NULL . 8)) . NIL . NIL . NIL . (13) . NIL . LISP . NIL .
NIL . 13 .) ((((∀ X U)) (¬ (NULL (CONS X U)))) . (AXIOM (TM& ((∀ X U)) (¬
(NULL (CONS X U))))) . NIL . ((U . 1) (X . 2) (CONS . 6) (NULL . 8)) . NIL
. NIL . NIL . (14) . NIL . LISP . NIL . NIL . 14 .) ((((∀ X U)) (= (CAR
(CONS X U)) X)) . (AXIOM (TM& ((∀ X U)) (= (CAR (CONS X U)) X))) . NIL .
((U . 1) (X . 2) (CONS . 6) (CAR . 7)) . NIL . NIL . NIL . (15) . NIL .
LISP . NIL . NIL . 15 .) ((((∀ X U)) (= (CDR (CONS X U)) U)) . (AXIOM (TM&
((∀ X U)) (= (CDR (CONS X U)) U))) . NIL . ((U . 1) (X . 2) (CONS . 6)
(CDR . 7)) . NIL . NIL . NIL . (16) . NIL . LISP . NIL . NIL . 16 .) ((((∀
PHI)) (⊃ (∧ (PHI NNIL) (((∀ X U)) (⊃ (PHI U) (PHI (CONS X U))))) (((∀ U))
(PHI U)))) . (AXIOM (TM& ((∀ PHI)) (⊃ (∧ (PHI NNIL) (((∀ X U)) (⊃ (PHI U)
(PHI (CONS X U))))) (((∀ U)) (PHI U))))) . NIL . ((U . 1) (X . 2) (PHI .
4) (NNIL . 5) (CONS . 6)) . NIL . NIL . NIL . (17) . NIL . LISP . NIL .
NIL . 17 .) (NIL . (DECL (*) (OT& (GROUND GROUND) . GROUND) CONSTANT NIL
INFIX 800) . NIL . ((* . (CONSTANT . ((GROUND GROUND) . GROUND) .
UNIVERSAL . NIL . (1 . * . INFIX . 800 .) . 18 . * .))) . NIL . NIL . NIL
. NIL . NIL . LISP . NIL . NIL . 18 .) ((((∀ U V)) (= (* U V) (CONDI (NULL
U) V (CONS (CAR U) (* (CDR U) V))))) . (AXIOM (TM& ((∀ U V)) (= (* U V)
(CONDI (NULL U) V (CONS (CAR U) (* (CDR U) V)))))) . NIL . ((V . 1) (U .
1) (CONS . 6) (CAR . 7) (CDR . 7) (NULL . 8) (* . 18)) . NIL . NIL . NIL .
(19) . NIL . LISP . NIL . NIL . 19 .) (NIL . (DECL (REVERSE LIST1) (OT&
(GROUND) . GROUND) CONSTANT) . NIL . ((LIST1 . (CONSTANT . ((GROUND) .
GROUND) . UNIVERSAL . NIL . NIL . 20 . LIST1 .)) (REVERSE . (CONSTANT .
((GROUND) . GROUND) . UNIVERSAL . NIL . NIL . 20 . REVERSE .))) . NIL .
NIL . NIL . NIL . NIL . LISP . NIL . NIL . 20 .) ((((∀ X)) (= (LIST1 X)
(CONS X NNIL))) . (AXIOM (TM& ((∀ X)) (= (LIST1 X) (CONS X NNIL)))) . NIL
. ((X . 2) (NNIL . 5) (CONS . 6) (LIST1 . 20)) . NIL . NIL . NIL . (21) .
NIL . LISP . NIL . NIL . 21 .) ((((∀ U)) (= (REVERSE U) (CONDI (NULL U)
NNIL (* (REVERSE (CDR U)) (LIST1 (CAR U)))))) . (AXIOM (TM& ((∀ U)) (=
(REVERSE U) (CONDI (NULL U) NNIL (* (REVERSE (CDR U)) (LIST1 (CAR U)))))))
. NIL . ((U . 1) (NNIL . 5) (CAR . 7) (CDR . 7) (NULL . 8) (* . 18)
(REVERSE . 20) (LIST1 . 20)) . NIL . NIL . NIL . (22) . NIL . LISP . NIL .
NIL . 22 .)))